﻿module BJK_ALGORITHM
open System

(* ANALYSIS OF EXPRESSIONS - in two versions *)
module Analysis =

    (* the purpose of these functions is to abstract an expression into a
       single column matrix, sorted! *)

    (*Input to analysis type *)
    type ANALYSIS_PARMS =
        abstract member nonlinear_Dvalue: AbstractDomain.abstractValue
        abstract member name: string

    type analysis(analysis_kind : ANALYSIS_PARMS) =
         (* abstract addition of 'columns' *)
        let add' d = AbstractDomain.lub AbstractDomain.additive d
        let add'' (i,d) = (i, add' d)

        let rec add = function
            | ([], ys) -> List.map add'' ys
            | (xs, []) -> List.map add'' xs
            | ((((i,d)::xt)as xs), (((i',d')::yt) as ys)) ->
                    if i=i' then (i, AbstractDomain.sum d d') :: add(xt,yt)
                    elif i<i' then (i,add' d) :: add(xt,ys)
                    else (i',add' d') :: add(xs,yt)

        (* utility functions: collect the variables in an Expr, or find the highest *)
        let rec merge = function
            | ([],ys) -> ys
            | (xs,[]) -> xs
            | (((x::xt) as xs), ((y::yt) as ys)) ->
                    if x=y then x::(merge(xt,yt))
                    elif x<y then x::(merge(xt,ys))
                    else y::(merge(xs,yt))

        let rec highest_var_inE = function
            | Core.Var i         -> i
            | Core.Plus(e1, e2)  -> max (highest_var_inE e1) (highest_var_inE e2)
            | Core.Times(e1, e2) -> max (highest_var_inE e1) (highest_var_inE e2)
            | Core.Zero          -> 1;

        let rec vars = function
            | Core.Var i         -> [i]
            | Core.Plus(e1, e2)  -> merge(vars e1, vars e2)
            | Core.Times(e1, e2) -> merge(vars e1, vars e2)
            | Core.Zero          -> []

        let rec highest_var = function
            | Core.Skip          -> 1
            | Core.Asgn(j,e)     -> max j (highest_var_inE e)
            | Core.Seq(C1,C2)    -> max (highest_var C1) (highest_var C2)
            | Core.Choice(C1,C2) -> max (highest_var C1) (highest_var C2)
            | Core.Loop(l,C)     -> max l (highest_var C);

        (* analyse an expression.  *)
        let rec analyseE = function
            | Core.Var i                 -> [(i,AbstractDomain.copy)]
            | Core.Plus(e1, e2)          -> add(analyseE e1, analyseE e2)
            | ((Core.Times( _, _)) as e) -> List.map (fun i -> (i, analysis_kind.nonlinear_Dvalue)) (vars e)
            | Core.Zero                  -> failwith "BJK.Analysis.analysis: Zero assignment is unsupported."

        (* main function: analyse a command *)
        member x.analyse(c) =
            let vars = highest_var c;

            let rec analyseC = function
                | Core.Skip          -> setOfPairs.dfrI(vars,Pattern.Cmd(-1))
                | Core.Asgn(j,e)     ->
                        let col = (List.map (fun (i,r) -> (i,j,r,Pattern.Cmd(-1))) (analyseE e));
                        let m = sparseMatrix.ins_in_I(vars,j,col)
                        setOfPairs.Dfr(m,sparseMatrix.r(m))
                | Core.Seq(C1,C2)    -> setOfPairs.prod(analyseC C1, analyseC C2)
                | Core.Choice(C1,C2) -> setOfPairs.sqcup(analyseC C1, analyseC C2)
                | Core.Loop(l,C)     -> setOfPairs.loop(l,vars,analysis_kind.nonlinear_Dvalue,(analyseC C),-1);

            analyseC c

        member x.resultText(c, dfr) =
            let vars = highest_var c
            match dfr with
                setOfPairs.Dfr(M, R) ->
                    let rec prt_ints = function
                        | [] -> "\n"
                        | i::rest -> (i.ToString()) + (if rest<>[] then ", " + (prt_ints rest) else "\n")

                    let (nonbounded, bounded) = sparseMatrix.classify(M,vars, AbstractDomain.exponentialAtLeast)
                    (setOfPairs.prtDfr(dfr) + "\n\nVARS: " + (vars.ToString()) + "\n" + analysis_kind.name + ": " +
                     (prt_ints bounded) + ("NON-" + analysis_kind.name + ": ") + (prt_ints nonbounded))

    (* analysis *)

    type PolyParams() =
         interface ANALYSIS_PARMS with
             member this.nonlinear_Dvalue = AbstractDomain.polynomial
             member this.name = "POLYNOMIAL"

    type LinParams() =
         interface ANALYSIS_PARMS with
             member this.nonlinear_Dvalue = AbstractDomain.exponentialAtLeast
             member this.name = "LINEAR"

    let Pol = analysis(PolyParams())

    let Lin = analysis(LinParams());